
(*       ___                                                              *)
(*      ||M||                                                             *)
(*      ||A||       A project by Andrea Asperti                           *)
(*      ||T||                                                             *)
(*      ||I||       Developers:                                           *)
(*      ||T||         The HELM team.                                      *)
(*      ||A||         http://helm.cs.unibo.it                             *)
(*      \   /                                                             *)
(*       \ /        This file is distributed under the terms of the       *)
(*        v         GNU General Public License Version 2                  *)
(*                                                                        *)
(**************************************************************************)

include "basics/logic.ma".
include "structures.ma".

(* MLLdi: down fragment. 
   Rule R T has R as conclusion and T as premise. 
   So, it derives R from T. *)
inductive Rule : Structure → Structure → Prop ≝ 
(* base cases *) 
| RuleAiD : ∀n    . Rule ((𝔸 \sub n) ⊠ (𝔹 \sub n)) 𝟙
| RuleSwi : ∀R,T,U. Rule ((R ⊗ U) ⊠ T) ((R ⊠ T) ⊗ U)
| RuleMix : ∀R,T  . Rule (R ⊠ T) (R ⊗ T) 
(* contextual closure *) 
| RuleNeg : ∀R,T  . Rule R T → Rule (Neg R) (Neg T)
| RuleParL: ∀R,T,U. Rule R T → Rule (R ⊠ U) (T ⊠ U)
| RuleParR: ∀R,T,U. Rule R T → Rule (U ⊠ R) (U ⊠ T)
| RuleCopL: ∀R,T,U. Rule R T → Rule (R ⊗ U) (T ⊗ U)
| RuleCopR: ∀R,T,U. Rule R T → Rule (U ⊗ R) (U ⊗ T)
(* *)
| RuleRefl:∀ R    . Rule R R
| RuleTran:∀ R,U,T. Rule R U → Rule U T → Rule R T 
(* closure up to the equivalence on structures *) 
| RuleMor: ∀R,T,U,V. (R = U) → (T = V) → (Rule R T) → (Rule U V).

definition RuleMorph: binary_morphism Structure Structure PROP.
 % 1
 [ @Rule
 | #H8 #H9 #H10 #H11 #H12 #H13 %;  
   [ @(RuleMor H8 H10 H9 H11) [ assumption | assumption ] 
   | @(RuleMor H9 H11 H8 H10) [ @(EqRelFormula_is_Sym H8 H9); assumption 
                               | @(EqRelFormula_is_Sym H10 H11); assumption ]
   ] ] qed . 

(* Contextual closure of Rule 
inductive RuleCntx : Structure → Structure → Prop ≝
| RuleCntxRfl : ∀R    . RuleCntx R R
| RuleCntxLift: ∀R,T  . Rule     R T → RuleCntx R T
| RuleCntxNeg : ∀R,T  . RuleCntx R T → RuleCntx (Neg R) (Neg T)
| RuleCntxParL: ∀R,T,U. RuleCntx R T → RuleCntx (R ⊠ U) (T ⊠ U)
| RuleCntxParR: ∀R,T,U. RuleCntx R T → RuleCntx (U ⊠ R) (U ⊠ T)
| RuleCntxCopL: ∀R,T,U. RuleCntx R T → RuleCntx (R ⊗ U) (T ⊗ U)
| RuleCntxCopR: ∀R,T,U. RuleCntx R T → RuleCntx (U ⊗ R) (U ⊗ T) .

lemma RuleMorphCntx: binary_morphism Structure Structure PROP.
 constructor 1
 [ apply RuleCntx
 | intros; split; intro; elim a'; elim b'
   [1: apply RuleCntxLift;
   |2:
   ]
 ] qed . 
*)

(* MLLdi: reflexive and transitive closure of Rule. 
inductive MLLdi: Structure → Structure → Prop ≝
| MLLdiRefl:∀ R    . MLLdi R R
| MLLdiLift:∀ R,T  . Rule  R T → MLLdi R T
| MLLdiTran:∀ R,U,T. MLLdi R U → MLLdi U T → MLLdi R T .
*)

(* MLLdi: notation and interpretation *)
notation "hvbox(T ⊢ R)" with precedence 45 for @{ 'Rule $R $T }.
interpretation "MLL" 'Rule R T = (Rule R T).

lemma MLL: binary_morphism Structure Structure PROP.
 % 1
 [ @Rule
 | #H15 #H16 #H17 #H18 #H19 #H20 % 
   [1: #H22 @(RuleMor H15 H17 H16 H18); [ assumption | assumption | assumption ]
   |2: @(RuleMor H16 H18 H15  H17); [ @EqRelFormula_is_Sym; assumption 
                                   | @EqRelFormula_is_Sym; ] assumption 
                                   ]]
   qed. 

(***** Lifting the behaviour of the rules to MLLdi ****)
(* Base cases *)
lemma MLLdiRuleAiD: ∀n. 𝟙   ⊢ ((𝔸 \sub n) ⊠ (𝔹 \sub n)).
#H24 @RuleAiD. qed.

lemma MLLdiRuleSwi: ∀R,T,U. ((R ⊠ T) ⊗ U) ⊢ ((R ⊗ U) ⊠ T).
#H26 #H27 #H28 @RuleSwi. qed.

  lemma MLLdiRuleParUnit    : ∀ R. R ⊢ (𝟙 ⊠ R).
#R
@(RuleMor (𝟙 ⊠ R) (𝟙 ⊠ R) ? R);
// normalize; @EqFormulaLift;
    @CntFormulaLift; @RelFormulaParUnit qed.

lemma MLLdiRuleParUnitRev    : ∀ R. 𝟙 ⊠ R ⊢ R .
#R
@(RuleMor R R ? (𝟙 ⊠ R))
//
normalize @EqFormulaLift; @CntFormulaLift; @RelFormulaComm; @RelFormulaParUnit
qed.


(* Le due proprietà MLLdiRuleParUnit e MLLdiRuleParUnitRev appena dimostrate 
   implicano che  R e (𝟙 ⊠ R)  sono equiprovabili. Mi sarei aspettato meno
   lavoro per dimostrarlo. Forse, manca qualcosa. Ad esempio Rule definisce
   le regole, però, non una dimostrazione, che è:
   1) una formula
   2) una regola
   3) la conposizione di sequenze di derivazioni
*)




lemma MLLdiRuleSwi2: ∀R,T,U. (U ⊗ (R ⊠ T)) ⊢ ((R ⊗ U) ⊠ T).
#R #T #U
@(RuleMor (ParMorph (R ⊗ U) T) 
               ((ParMorph R T) ⊗ U) 
               ? (* Can be equal to (ParMorph (R ⊗ U) T) *)
               (U ⊗ (ParMorph R T)) );               
[1: whd; //;
|3: @RuleSwi;
|2: normalize; @EqFormula_is_Sym; 
    @( EqFormula_is_Tran ? ((R ⊗ U) ⊠ T) ?); 
    normalize;
    [1: @EqFormulaLift;
    |2: @ (* Non riesco a procedere perché mi occorre 
    ];
apply R;
apply RuleSwi. qed.



lemma MLLdiRuleMix: ∀R,T,U. (R ⊗ T) ⊢ (R ⊠ U).
intros; apply RuleMix.  qed.

(* unit *)
lemma MLLdiRuleUnitParUnit: 𝟙 ⊢ (𝟙  ⊠ 𝟙^⊥).
 apply (RuleMor 𝟙 𝟙 ? ?)
 [1: (* potrebbe servire il lifting del test in structures.ma *)
 |2:
 |3:
 ]


lemma MLLdiRuleUnitParUnit: 𝟙 ⊢ (𝟙  ⊠ 𝟙).
 apply (RuleTran ? (𝟙 ⊠ 𝟙^⊥) ? );
 [1: apply (RuleMor (𝟙 ⊠ 𝟙) (𝟙 ⊠ 𝟙) (𝟙 ⊠ 𝟙) (𝟙 ⊠ 𝟙^⊥))
 |2: apply MLLdiRuleAiD;
 ]

lemma MLLdiRuleCopUnit    : ∀ R. R ⊢ (𝟙  ⊗ R).
intros; apply MLLdiLift; autobatch. qed.

lemma MLLdiRuleParUnitInv : ∀ R. (𝟙 ⊠ R) ⊢ R.
intros; apply MLLdiLift; autobatch. qed.

lemma MLLdiRuleCopUnitInv : ∀ R. (𝟙  ⊗ R) ⊢ R.
intros; apply MLLdiLift; autobatch. qed.

(* associativity from left to right *)
lemma MLLdiRuleParAsc: ∀ R,T,U. R ⊠ T ⊠ U ⊢ R ⊠ (T ⊠ U).
intros; apply MLLdiLift; autobatch. qed.

lemma MLLdiRuleCopAsc: ∀ R,T,U. R ⊗ T ⊗ U ⊢ R ⊗ (T ⊗ U).
intros; apply MLLdiLift; autobatch. qed.

(* commutativity *)
lemma MLLdiRuleParCom: ∀ R,T. R ⊠ T ⊢ T ⊠ R.
intros; apply MLLdiLift; autobatch. qed.

lemma MLLdiRuleCopCom: ∀ R,T. R ⊗ T ⊢ T ⊗ R.
intros; apply MLLdiLift; autobatch. qed.

(***** Symmetry of the above lifting *******)
(* Sym base cases *)
lemma MLLdiRuleAiDSym: ∀n. 𝟙   ⊢ ((𝔹 \sub n) ⊠ (𝔸 \sub n)).
intros; apply (MLLdiTran ? ? ((Atom n) ⊠ (NAtom n)));
normalize; autobatch. qed.

lemma MLLdiRuleSwiSym: ∀R,T,U. ((R ⊠ T) ⊗ U) ⊢ (T ⊠ (R ⊗ U)).
intros; apply (MLLdiTran ? ? ((R ⊗ U) ⊠ T));
normalize; autobatch. qed.

lemma MLLdiRuleMixSym: ∀R,T,U. (R ⊗ T) ⊢ (U ⊠ R).
intros; apply (MLLdiTran ? ? (R ⊠ U));
normalize; autobatch. qed.

(* Sym unit *) 
lemma MLLdiRuleParUnitSym    : ∀ R. R ⊢ (R ⊠ 𝟙).
intros; apply (MLLdiTran ? ? (𝟙 ⊠ R));
normalize; autobatch. qed.

lemma MLLdiRuleCopUnitSym    : ∀ R. R ⊢ (R ⊗ 𝟙).
intros; apply (MLLdiTran ? ? (𝟙  ⊗ R));
normalize; autobatch. qed.

lemma MLLdiRuleParUnitInvSym    : ∀ R. (R ⊠ 𝟙) ⊢ R.
intros; apply (MLLdiTran ? ? (𝟙 ⊠ R));
normalize; autobatch. qed.

lemma MLLdiRuleCopUnitInvSym    : ∀ R. (R ⊗ 𝟙) ⊢ R.
intros; apply (MLLdiTran ? ? (𝟙  ⊗ R));
normalize; autobatch. qed.

(* Sym associativity from left to right *)
lemma MLLdiRuleParAscSym: ∀ R,T,U. R ⊠ T ⊠ U ⊢ (T ⊠ U) ⊠ R.
intros; apply (MLLdiTran ? ? (R ⊠ (T ⊠ U)));
normalize; autobatch. qed.

lemma MLLdiRuleCopAscSym: ∀ R,T,U. R ⊗ T ⊗ U ⊢ (T ⊗ U) ⊗ R.
intros; apply (MLLdiTran ? ? (R ⊗ (T ⊗ U)));
normalize; autobatch. qed.

(***** Lifting the behaviour of the contexts to MLLdi ****)
lemma MLLdiCntxParL  :  ∀ R,T,U. T ⊢ R → (U ⊠ T) ⊢ (U ⊠ R).
intros; elim H;
[1: apply MLLdiRefl
|2: apply MLLdiLift; apply RuleCntxParR; assumption
|3: apply (MLLdiTran ? ? (U ⊠ f2)); assumption;
] qed.

lemma MLLdiCntxParR: ∀ R,T,U. T ⊢ R →  (T ⊠ U) ⊢ (R ⊠ U).
(* LR: the proof of MLLdiCntxParL could be like the
       following one *)
intros; elim H; autobatch. qed.

lemma MLLdiCntxCopL: ∀ R,T,U. T ⊢ R →  (U ⊗ T) ⊢ (U ⊗ R).
intros; elim H; autobatch. qed.

lemma MLLdiCntxCopR: ∀ R,T,U. T ⊢ R →  (T ⊗ U) ⊢ (R ⊗ U).
intros; elim H; autobatch. qed.

lemma MLLdiCntxPar: ∀ R,T,U,V. T ⊢ R → V ⊢ U → (T ⊠ V) ⊢ (R ⊠ U).
intros; elim H; 
[1: apply MLLdiCntxParL; assumption
|2: lapply (MLLdiLift f f1) [2: assumption 
                            |1: autobatch (* induction *)]
|3: try autobatch (* induction *) ] qed.

lemma MLLdiCntxCop: ∀ R,T,U,V. T ⊢ R → V ⊢ U → (T ⊗ V) ⊢ (R ⊗ U).
intros; elim H; 
[1: apply MLLdiCntxCopL; assumption
|2: lapply (MLLdiLift f f1) [2: assumption 
                            |1: autobatch (* induction *)]
|3: try autobatch (* induction *) ] qed.

(***** General unit down derivable ****)
lemma MLLdiUnitPar: 𝟙  ⊢ 𝟙  ⊠ 𝟙 .
apply MLLdiRuleParUnit. qed.

lemma MLLdiUnitCop: 𝟙  ⊢ 𝟙  ⊗ 𝟙 .
apply MLLdiRuleCopUnit. qed.

(***** General axiom interaction down derivable ****)
lemma MLLdiAiD: ∀ R. 𝟙  ⊢ R ⊠ (R^⊥).
intro; elim R; simplify; 
[1: apply MLLdiRuleAiD;
|2: apply (MLLdiTran ((𝔹\sub n) ⊠ (𝔸\sub n)) (*R*)
                                          𝟙                                               (*T*)
                     ((𝔸\sub n) ⊠ (𝔹\sub n)) (*U*)); 
    [2: apply MLLdiRuleAiD 
    |1: apply MLLdiRuleParCom ]
|3: apply MLLdiUnitPar
|4: apply (MLLdiTran ?(*R*) ?(*T*) (𝟙 ⊗𝟙)(*U*));
    [1:apply (MLLdiTran ?(*R*) ?(*T*)
                      ((f1 ⊠ f1^⊥) ⊗ (f ⊠ f^⊥))(*U*))
        [2: autobatch (* applies the inductive 
                         hypothesis H and H1 *) 
        |1: apply (MLLdiTran ? ? (((f ⊗ f1) ⊠ f^⊥) ⊠ f1^⊥))
            [1: apply MLLdiRuleParAsc;
            |2: apply (MLLdiTran ? ? (((f ⊠ f^⊥) ⊗ f1) ⊠ f1^⊥))
                [1: apply MLLdiCntxParR; apply MLLdiRuleSwi
                |2: try autobatch
                ]
            ]
        ]
    |2: apply MLLdiUnitCop ]
|5: apply (MLLdiTran ?(*R*) 𝟙(*T*) ((f^⊥ ⊗ f1^⊥) ⊠ (f ⊠ f1))(*U*))
    [1: apply MLLdiRuleParCom
    |2: apply (MLLdiTran ?(*R*) ?(*T*) (𝟙 ⊗𝟙)(*U*));
        [1: apply (MLLdiTran ?(*R*) ?(*T*)
                      ((f1^⊥ ⊠ f1) ⊗ (f^⊥ ⊠ f))(*U*))
            [1: apply (MLLdiTran ? ? (((f^⊥ ⊗ f1^⊥) ⊠ f) ⊠ f1))
                [1: apply MLLdiRuleParAsc;
                |2: apply (MLLdiTran ? ? (((f^⊥ ⊠ f) ⊗ f1^⊥) ⊠ f1))
                    [1: apply MLLdiCntxParR; apply MLLdiRuleSwi
                    |2: try autobatch
                    ]
                ]
            |2: try autobatch (* applies the inductive 
                                 hypothesis H and H1, 
                                 exploiting MLLdiCntxCop *) 
            ]
        |2: apply MLLdiUnitCop ]
    ]
] qed .

(* CSC: stai dimostrando MLLdi_ind gia' dimostrato automaticamente.
   Il lemma MLLdiElim e' troppo debole perche' non ottieni ipotesi
   induttive su  T ⊢ U e U ⊢ R. Di fatto il tuo MLLdiElim e' solo
   case analysis, mentre Minimality e' un lemma piu' forte di induzione.
   Eccolo dimostrato (banalmente) usando MLLdi_ind che ha lo stesso
   enunciato. *)
lemma MLLdiMinimality:
∀ P:Formula → Formula → Prop. 
  (∀ R    . P R R)
→ (∀ R,T  . RuleCntx R T → P R T)
→ (∀ R,U,T. U ⊢ R → P R U → T ⊢ U → P U T → P R T)
→ (∀ R,T  . T ⊢ R → P R T).
intros;
elim H3  
 [1: apply H
 |2: apply H1; apply H4
 |3: apply (H2 f    (* R *)
               f2   (* U *)
               f1   (* T *)
           )  (* The essential goal could
                 also be "apply (H2 ? s2)"  *)     
    [ assumption (* H4 *)
    | assumption (* H5 *)
    | assumption (* H6 *)
    | assumption (* H7 *)
    ]
 ]
qed.
